Nuprl Definition : assoc 13,42
basic
Assoc(T;op) == x, y, z:T. (x op (y op z)) = ((x op y) op z) 
latex

clarification:

basic
Assoc(T;op) == x:T. y:T, z:T. (x op (y op z)) = ((x op y) op z)  T 
latex

Upgen algebra 1
Wellformedness Lemmasassoc wf
Definitionsx:A. B(x), x f y

origin